Termination w.r.t. Q proof of TRS/secret05cime5.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> U'15'1₁(intersect'ii'in₂(F1, F2))
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> U'1'1₁(intersect'ii'in₂(Xs, Ys))
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> U'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> U'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> U'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> U'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> U'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right))
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> U'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> U'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> U'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> U'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> INTERSECT'II'IN₂(Xs, Ys)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> U'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> U'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F2, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> INTERSECT'II'IN₂(F1, F2)
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> U'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, Fs), Gs), NF)
INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> U'2'1₁(intersect'ii'in₂(Xs, Ys))
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> U'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
TAUTOLOGY'I'IN₁(F) -> REDUCE'II'IN₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> U'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
TAUTOLOGY'I'IN₁(F) -> U'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> U'15'1₁(intersect'ii'in₂(F1, F2))
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> U'1'1₁(intersect'ii'in₂(Xs, Ys))
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> U'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> U'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> U'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> U'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> U'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right))
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> U'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> U'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> U'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> U'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> INTERSECT'II'IN₂(Xs, Ys)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> U'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> U'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F2, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> INTERSECT'II'IN₂(F1, F2)
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> U'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, Fs), Gs), NF)
INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> U'2'1₁(intersect'ii'in₂(Xs, Ys))
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> U'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
TAUTOLOGY'I'IN₁(F) -> REDUCE'II'IN₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil))
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> U'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
TAUTOLOGY'I'IN₁(F) -> U'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 18 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> INTERSECT'II'IN₂(Xs, Ys)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

INTERSECT'II'IN₂(cons₂(X0, Xs), Ys) -> INTERSECT'II'IN₂(Xs, Ys)
INTERSECT'II'IN₂(Xs, cons₂(X0, Ys)) -> INTERSECT'II'IN₂(Xs, Ys)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(INTERSECT'II'IN₂(x₁, x₂)) = 3·x₁ + 3·x₂
POL(cons₂(x₁, x₂)) = 3 + x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> U'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F2, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> U'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right))
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> U'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
REDUCE'II'IN₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right)))
REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> U'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
REDUCE'II'IN₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> REDUCE'II'IN₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right))

The remaining pairs can at least be oriented weakly.

REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F2, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

Used ordering: Polynomial interpretation [21]:

POL(REDUCE'II'IN₂(x₁, x₂)) = 2 + x₁
POL(U'12'1₅(x₁, x₂, x₃, x₄, x₅)) = 3 + 2·x₁ + x₂ + 2·x₃ + x₄
POL(U'6'1₅(x₁, x₂, x₃, x₄, x₅)) = 3 + 2·x₁ + 2·x₂ + x₃ + x₄
POL(cons₂(x₁, x₂)) = 2 + 2·x₁ + x₂
POL(if₂(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(iff₂(x₁, x₂)) = 3 + 3·x₁ + 3·x₂
POL(intersect'ii'in₂(x₁, x₂)) = 0
POL(intersect'ii'out) = 1
POL(nil) = 0
POL(p₁(x₁)) = 2
POL(reduce'ii'in₂(x₁, x₂)) = 2
POL(reduce'ii'out) = 2
POL(sequent₂(x₁, x₂)) = 3 + x₁ + x₂
POL(u'1'1₁(x₁)) = 0
POL(u'10'1₁(x₁)) = 2
POL(u'11'1₁(x₁)) = 2
POL(u'12'1₅(x₁, x₂, x₃, x₄, x₅)) = x₁
POL(u'12'2₁(x₁)) = 2
POL(u'13'1₁(x₁)) = x₁
POL(u'14'1₁(x₁)) = 2
POL(u'15'1₁(x₁)) = 3·x₁
POL(u'2'1₁(x₁)) = 0
POL(u'3'1₁(x₁)) = 2
POL(u'4'1₁(x₁)) = 2
POL(u'5'1₁(x₁)) = 2
POL(u'6'1₅(x₁, x₂, x₃, x₄, x₅)) = x₁
POL(u'6'2₁(x₁)) = 2
POL(u'7'1₁(x₁)) = 2
POL(u'8'1₁(x₁)) = 2
POL(u'9'1₁(x₁)) = 2
POL(x'2a₂(x₁, x₂)) = 1 + x₁ + x₂
POL(x'2b₂(x₁, x₂)) = 1 + 2·x₁ + x₂
POL(x'2d₁(x₁)) = x₁

The following usable rules [14] were oriented:

reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
u'6'2₁(reduce'ii'out) -> reduce'ii'out
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'7'1₁(reduce'ii'out) -> reduce'ii'out
u'14'1₁(reduce'ii'out) -> reduce'ii'out
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
U'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F2, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)
U'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G2, Gs)), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 2 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ QDP

                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF)

The remaining pairs can at least be oriented weakly.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

Used ordering: Polynomial interpretation [21]:

POL(REDUCE'II'IN₂(x₁, x₂)) = x₁
POL(cons₂(x₁, x₂)) = x₁ + x₂
POL(if₂(x₁, x₂)) = x₁ + 2·x₂
POL(iff₂(x₁, x₂)) = 1 + 3·x₁ + 3·x₂
POL(sequent₂(x₁, x₂)) = 2·x₁ + 3·x₂
POL(x'2a₂(x₁, x₂)) = x₁ + x₂
POL(x'2b₂(x₁, x₂)) = x₁ + x₂
POL(x'2d₁(x₁)) = 2·x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(G1, Fs), Gs), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(F1, Gs)), NF)
REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF)
REDUCE'II'IN₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF)

The remaining pairs can at least be oriented weakly.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

Used ordering: Polynomial interpretation [21]:

POL(REDUCE'II'IN₂(x₁, x₂)) = 3·x₁
POL(cons₂(x₁, x₂)) = 1 + 3·x₁ + x₂
POL(if₂(x₁, x₂)) = 2 + 3·x₁ + 2·x₂
POL(sequent₂(x₁, x₂)) = x₁ + x₂
POL(x'2a₂(x₁, x₂)) = 2 + x₁ + x₂
POL(x'2b₂(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(x'2d₁(x₁)) = 1 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

REDUCE'II'IN₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> REDUCE'II'IN₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF)
REDUCE'II'IN₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> REDUCE'II'IN₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(REDUCE'II'IN₂(x₁, x₂)) = 3·x₁
POL(cons₂(x₁, x₂)) = 3·x₁
POL(if₂(x₁, x₂)) = 2 + x₁ + 3·x₂
POL(sequent₂(x₁, x₂)) = 3·x₁ + 2·x₂
POL(x'2b₂(x₁, x₂)) = x₁ + x₂
POL(x'2d₁(x₁)) = 1

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ DependencyGraphProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ QDPOrderProof

                              ↳ QDP

                                ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

intersect'ii'in₂(cons₂(X, X0), cons₂(X, X1)) -> intersect'ii'out
intersect'ii'in₂(Xs, cons₂(X0, Ys)) -> u'1'1₁(intersect'ii'in₂(Xs, Ys))
u'1'1₁(intersect'ii'out) -> intersect'ii'out
intersect'ii'in₂(cons₂(X0, Xs), Ys) -> u'2'1₁(intersect'ii'in₂(Xs, Ys))
u'2'1₁(intersect'ii'out) -> intersect'ii'out
reduce'ii'in₂(sequent₂(cons₂(if₂(A, B), Fs), Gs), NF) -> u'3'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2b₂(x'2d₁(B), A), Fs), Gs), NF))
u'3'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(iff₂(A, B), Fs), Gs), NF) -> u'4'1₁(reduce'ii'in₂(sequent₂(cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Fs), Gs), NF))
u'4'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2a₂(F1, F2), Fs), Gs), NF) -> u'5'1₁(reduce'ii'in₂(sequent₂(cons₂(F1, cons₂(F2, Fs)), Gs), NF))
u'5'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2b₂(F1, F2), Fs), Gs), NF) -> u'6'1₅(reduce'ii'in₂(sequent₂(cons₂(F1, Fs), Gs), NF), F2, Fs, Gs, NF)
u'6'1₅(reduce'ii'out, F2, Fs, Gs, NF) -> u'6'2₁(reduce'ii'in₂(sequent₂(cons₂(F2, Fs), Gs), NF))
u'6'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(x'2d₁(F1), Fs), Gs), NF) -> u'7'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(F1, Gs)), NF))
u'7'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(if₂(A, B), Gs)), NF) -> u'8'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(x'2d₁(B), A), Gs)), NF))
u'8'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(iff₂(A, B), Gs)), NF) -> u'9'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(if₂(A, B), if₂(B, A)), Gs)), NF))
u'9'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(cons₂(p₁(V), Fs), Gs), sequent₂(Left, Right)) -> u'10'1₁(reduce'ii'in₂(sequent₂(Fs, Gs), sequent₂(cons₂(p₁(V), Left), Right)))
u'10'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2b₂(G1, G2), Gs)), NF) -> u'11'1₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, cons₂(G2, Gs))), NF))
u'11'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2a₂(G1, G2), Gs)), NF) -> u'12'1₅(reduce'ii'in₂(sequent₂(Fs, cons₂(G1, Gs)), NF), Fs, G2, Gs, NF)
u'12'1₅(reduce'ii'out, Fs, G2, Gs, NF) -> u'12'2₁(reduce'ii'in₂(sequent₂(Fs, cons₂(G2, Gs)), NF))
u'12'2₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(Fs, cons₂(x'2d₁(G1), Gs)), NF) -> u'13'1₁(reduce'ii'in₂(sequent₂(cons₂(G1, Fs), Gs), NF))
u'13'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, cons₂(p₁(V), Gs)), sequent₂(Left, Right)) -> u'14'1₁(reduce'ii'in₂(sequent₂(nil, Gs), sequent₂(Left, cons₂(p₁(V), Right))))
u'14'1₁(reduce'ii'out) -> reduce'ii'out
reduce'ii'in₂(sequent₂(nil, nil), sequent₂(F1, F2)) -> u'15'1₁(intersect'ii'in₂(F1, F2))
u'15'1₁(intersect'ii'out) -> reduce'ii'out
tautology'i'in₁(F) -> u'16'1₁(reduce'ii'in₂(sequent₂(nil, cons₂(F, nil)), sequent₂(nil, nil)))
u'16'1₁(reduce'ii'out) -> tautology'i'out

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.